

LEMMA

External connection implies connection.
=============================
Step 1

? (all x (all y ((ec x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (ec c29326 c29325)) v (c c29326 c29325))


> hypdisj
=============================
Step 3

? (c c29326 c29325)

1. (ec c29326 c29325)

> ((c X Y) <-- (ec X Y))
=============================
Step 4

? (ec c29326 c29325)

1. (~ (c c29326 c29325))
2. (ec c29326 c29325)

> hyp


LEMMA

Case split: x and z are either disconnected or connected.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (ec y z)) => ((dc x z) v (c x z))))))


> revsk
=============================
Step 2

? (((~ (ec c34457 c34456)) v (~ (ec c34456 c34455))) v ((dc c34457 c34455) v (c c34457 c34455)))


> hypdisj
=============================
Step 3

? (c c34457 c34455)

1. (~ (dc c34457 c34455))
2. (ec c34456 c34455)
3. (ec c34457 c34456)

> ((c X Y) <-- (~ (dc X Y)))
=============================
Step 4

? (~ (dc c34457 c34455))

1. (~ (c c34457 c34455))
2. (~ (dc c34457 c34455))
3. (ec c34456 c34455)
4. (ec c34457 c34456)

> hyp


LEMMA

If x and z are connected, split into external connection or overlap.
=============================
Step 1

? (all x (all y (all z ((((ec x y) & (ec y z)) & (c x z)) => ((ec x z) v (o x z))))))


> revsk
=============================
Step 2

? ((((~ (ec c39854 c39853)) v (~ (ec c39853 c39852))) v (~ (c c39854 c39852))) v ((ec c39854 c39852) v (o c39854 c39852)))


> hypdisj
=============================
Step 3

? (o c39854 c39852)

1. (~ (ec c39854 c39852))
2. (c c39854 c39852)
3. (ec c39853 c39852)
4. (ec c39854 c39853)

> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|=============================
|Step 4
|
|? (c c39854 c39852)
|
|1. (~ (o c39854 c39852))
|2. (~ (ec c39854 c39852))
|3. (c c39854 c39852)
|4. (ec c39853 c39852)
|5. (ec c39854 c39853)
|
|> hyp
=============================
Step 5

? (~ (ec c39854 c39852))

1. (~ (o c39854 c39852))
2. (~ (ec c39854 c39852))
3. (c c39854 c39852)
4. (ec c39853 c39852)
5. (ec c39854 c39853)

> hyp


LEMMA

Overlap decomposes into po, pp, pp-1, or extensional equality.
=============================
Step 1

? (all x (all y ((o x y) => ((((po x y) v (pp x y)) v (pp-1 x y)) v (e= x y)))))


> revsk
=============================
Step 2

? ((~ (o c45665 c45664)) v ((((po c45665 c45664) v (pp c45665 c45664)) v (pp-1 c45665 c45664)) v (e= c45665 c45664)))


> hypdisj
=============================
Step 3

? (e= c45665 c45664)

1. (~ (pp-1 c45665 c45664))
2. (~ (pp c45665 c45664))
3. (~ (po c45665 c45664))
4. (o c45665 c45664)

> ((e= Y X) <-- (p Y X) (p X Y))
|=============================
|Step 4
|
|? (p c45665 c45664)
|
|1. (~ (e= c45665 c45664))
|2. (~ (pp-1 c45665 c45664))
|3. (~ (pp c45665 c45664))
|4. (~ (po c45665 c45664))
|5. (o c45665 c45664)
|
|> ((p Y X) <-- (p X Y) (~ (pp X Y)))
||=============================
||Step 5
||
||? (p c45664 c45665)
||
||1. (~ (p c45665 c45664))
||2. (~ (e= c45665 c45664))
||3. (~ (pp-1 c45665 c45664))
||4. (~ (pp c45665 c45664))
||5. (~ (po c45665 c45664))
||6. (o c45665 c45664)
||
||> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||||=============================
||||Step 6
||||
||||? (o c45665 c45664)
||||
||||1. (~ (p c45664 c45665))
||||2. (~ (p c45665 c45664))
||||3. (~ (e= c45665 c45664))
||||4. (~ (pp-1 c45665 c45664))
||||5. (~ (pp c45665 c45664))
||||6. (~ (po c45665 c45664))
||||7. (o c45665 c45664)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (~ (p c45665 c45664))
|||
|||1. (~ (p c45664 c45665))
|||2. (~ (p c45665 c45664))
|||3. (~ (e= c45665 c45664))
|||4. (~ (pp-1 c45665 c45664))
|||5. (~ (pp c45665 c45664))
|||6. (~ (po c45665 c45664))
|||7. (o c45665 c45664)
|||
|||> hyp
||=============================
||Step 8
||
||? (~ (po c45665 c45664))
||
||1. (~ (p c45664 c45665))
||2. (~ (p c45665 c45664))
||3. (~ (e= c45665 c45664))
||4. (~ (pp-1 c45665 c45664))
||5. (~ (pp c45665 c45664))
||6. (~ (po c45665 c45664))
||7. (o c45665 c45664)
||
||> hyp
|=============================
|Step 9
|
|? (~ (pp c45664 c45665))
|
|1. (~ (p c45665 c45664))
|2. (~ (e= c45665 c45664))
|3. (~ (pp-1 c45665 c45664))
|4. (~ (pp c45665 c45664))
|5. (~ (po c45665 c45664))
|6. (o c45665 c45664)
|
|> ((~ (pp Y X)) <-- (~ (pp-1 X Y)))
|=============================
|Step 10
|
|? (~ (pp-1 c45665 c45664))
|
|1. (pp c45664 c45665)
|2. (~ (p c45665 c45664))
|3. (~ (e= c45665 c45664))
|4. (~ (pp-1 c45665 c45664))
|5. (~ (pp c45665 c45664))
|6. (~ (po c45665 c45664))
|7. (o c45665 c45664)
|
|> hyp
=============================
Step 11

? (p c45664 c45665)

1. (~ (e= c45665 c45664))
2. (~ (pp-1 c45665 c45664))
3. (~ (pp c45665 c45664))
4. (~ (po c45665 c45664))
5. (o c45665 c45664)

> ((p Y X) <-- (p X Y) (~ (pp X Y)))
|=============================
|Step 12
|
|? (p c45665 c45664)
|
|1. (~ (p c45664 c45665))
|2. (~ (e= c45665 c45664))
|3. (~ (pp-1 c45665 c45664))
|4. (~ (pp c45665 c45664))
|5. (~ (po c45665 c45664))
|6. (o c45665 c45664)
|
|> ((p X Y) <-- (o X Y) (~ (p Y X)) (~ (po X Y)))
|||=============================
|||Step 13
|||
|||? (o c45665 c45664)
|||
|||1. (~ (p c45665 c45664))
|||2. (~ (p c45664 c45665))
|||3. (~ (e= c45665 c45664))
|||4. (~ (pp-1 c45665 c45664))
|||5. (~ (pp c45665 c45664))
|||6. (~ (po c45665 c45664))
|||7. (o c45665 c45664)
|||
|||> hyp
||=============================
||Step 14
||
||? (~ (p c45664 c45665))
||
||1. (~ (p c45665 c45664))
||2. (~ (p c45664 c45665))
||3. (~ (e= c45665 c45664))
||4. (~ (pp-1 c45665 c45664))
||5. (~ (pp c45665 c45664))
||6. (~ (po c45665 c45664))
||7. (o c45665 c45664)
||
||> hyp
|=============================
|Step 15
|
|? (~ (po c45665 c45664))
|
|1. (~ (p c45665 c45664))
|2. (~ (p c45664 c45665))
|3. (~ (e= c45665 c45664))
|4. (~ (pp-1 c45665 c45664))
|5. (~ (pp c45665 c45664))
|6. (~ (po c45665 c45664))
|7. (o c45665 c45664)
|
|> hyp
=============================
Step 16

? (~ (pp c45665 c45664))

1. (~ (p c45664 c45665))
2. (~ (e= c45665 c45664))
3. (~ (pp-1 c45665 c45664))
4. (~ (pp c45665 c45664))
5. (~ (po c45665 c45664))
6. (o c45665 c45664)

> hyp


LEMMA

Lift the overlap decomposition into the ec/ec context.
=============================
Step 1

? (all x (all y (all z (((((ec x y) & (ec y z)) & (c x z)) & (o x z)) => ((((po x z) v (pp x z)) v (pp-1 x z)) v (e= x z))))))


> revsk
=============================
Step 2

? (((((~ (ec c51887 c51886)) v (~ (ec c51886 c51885))) v (~ (c c51887 c51885))) v (~ (o c51887 c51885))) v ((((po c51887 c51885) v (pp c51887 c51885)) v (pp-1 c51887 c51885)) v (e= c51887 c51885)))


> hypdisj
=============================
Step 3

? (e= c51887 c51885)

1. (~ (pp-1 c51887 c51885))
2. (~ (pp c51887 c51885))
3. (~ (po c51887 c51885))
4. (o c51887 c51885)
5. (c c51887 c51885)
6. (ec c51886 c51885)
7. (ec c51887 c51886)

> ((e= X Y) <-- (o X Y) (~ (po X Y)) (~ (pp X Y)) (~ (pp-1 X Y)))
|||=============================
|||Step 4
|||
|||? (o c51887 c51885)
|||
|||1. (~ (e= c51887 c51885))
|||2. (~ (pp-1 c51887 c51885))
|||3. (~ (pp c51887 c51885))
|||4. (~ (po c51887 c51885))
|||5. (o c51887 c51885)
|||6. (c c51887 c51885)
|||7. (ec c51886 c51885)
|||8. (ec c51887 c51886)
|||
|||> hyp
||=============================
||Step 5
||
||? (~ (po c51887 c51885))
||
||1. (~ (e= c51887 c51885))
||2. (~ (pp-1 c51887 c51885))
||3. (~ (pp c51887 c51885))
||4. (~ (po c51887 c51885))
||5. (o c51887 c51885)
||6. (c c51887 c51885)
||7. (ec c51886 c51885)
||8. (ec c51887 c51886)
||
||> hyp
|=============================
|Step 6
|
|? (~ (pp c51887 c51885))
|
|1. (~ (e= c51887 c51885))
|2. (~ (pp-1 c51887 c51885))
|3. (~ (pp c51887 c51885))
|4. (~ (po c51887 c51885))
|5. (o c51887 c51885)
|6. (c c51887 c51885)
|7. (ec c51886 c51885)
|8. (ec c51887 c51886)
|
|> hyp
=============================
Step 7

? (~ (pp-1 c51887 c51885))

1. (~ (e= c51887 c51885))
2. (~ (pp-1 c51887 c51885))
3. (~ (pp c51887 c51885))
4. (~ (po c51887 c51885))
5. (o c51887 c51885)
6. (c c51887 c51885)
7. (ec c51886 c51885)
8. (ec c51887 c51886)

> hyp


LEMMA

Under ec/ec, proper part sharpens to tangential proper part.
=============================
Step 1

? (all x (all y (all z ((((ec x y) & (ec y z)) & (pp x z)) => (tpp x z)))))


> revsk
=============================
Step 2

? ((((~ (ec c59275 c59274)) v (~ (ec c59274 c59273))) v (~ (pp c59275 c59273))) v (tpp c59275 c59273))


> hypdisj
=============================
Step 3

? (tpp c59275 c59273)

1. (pp c59275 c59273)
2. (ec c59274 c59273)
3. (ec c59275 c59274)

> ((tpp X Z) <-- (pp X Z) (ec Y X) (ec Y Z))
||=============================
||Step 4
||
||? (pp c59275 c59273)
||
||1. (~ (tpp c59275 c59273))
||2. (pp c59275 c59273)
||3. (ec c59274 c59273)
||4. (ec c59275 c59274)
||
||> hyp
|=============================
|Step 5
|
|? (ec Var42 c59275)
|
|1. (~ (tpp c59275 c59273))
|2. (pp c59275 c59273)
|3. (ec c59274 c59273)
|4. (ec c59275 c59274)
|
|> ((ec X Y) <-- (c X Y) (~ (o X Y)))
||=============================
||Step 6
||
||? (c Var42 c59275)
||
||1. (~ (ec Var42 c59275))
||2. (~ (tpp c59275 c59273))
||3. (pp c59275 c59273)
||4. (ec c59274 c59273)
||5. (ec c59275 c59274)
||
||> ((c Y X) <-- (c X Y))
||=============================
||Step 7
||
||? (c c59275 Var42)
||
||1. (~ (c Var42 c59275))
||2. (~ (ec Var42 c59275))
||3. (~ (tpp c59275 c59273))
||4. (pp c59275 c59273)
||5. (ec c59274 c59273)
||6. (ec c59275 c59274)
||
||> ((c X Y) <-- (ec X Y))
||=============================
||Step 8
||
||? (ec c59275 Var42)
||
||1. (~ (c c59275 Var42))
||2. (~ (c Var42 c59275))
||3. (~ (ec Var42 c59275))
||4. (~ (tpp c59275 c59273))
||5. (pp c59275 c59273)
||6. (ec c59274 c59273)
||7. (ec c59275 c59274)
||
||> hyp
|=============================
|Step 9
|
|? (~ (o c59274 c59275))
|
|1. (~ (ec c59274 c59275))
|2. (~ (tpp c59275 c59273))
|3. (pp c59275 c59273)
|4. (ec c59274 c59273)
|5. (ec c59275 c59274)
|
|> ((~ (o Y X)) <-- (~ (p (f51952 Y X) Y)))
|=============================
|Step 10
|
|? (~ (p (f51952 c59274 c59275) c59274))
|
|1. (o c59274 c59275)
|2. (~ (ec c59274 c59275))
|3. (~ (tpp c59275 c59273))
|4. (pp c59275 c59273)
|5. (ec c59274 c59273)
|6. (ec c59275 c59274)
|
|> ((~ (p X Z)) <-- (p X Y) (~ (o Y Z)))
||=============================
||Step 11
||
||? (p (f51952 c59274 c59275) c59275)
||
||1. (p (f51952 c59274 c59275) c59274)
||2. (o c59274 c59275)
||3. (~ (ec c59274 c59275))
||4. (~ (tpp c59275 c59273))
||5. (pp c59275 c59273)
||6. (ec c59274 c59273)
||7. (ec c59275 c59274)
||
||> ((p (f51952 X Y) Y) <-- (o X Y))
||=============================
||Step 12
||
||? (o c59274 c59275)
||
||1. (~ (p (f51952 c59274 c59275) c59275))
||2. (p (f51952 c59274 c59275) c59274)
||3. (o c59274 c59275)
||4. (~ (ec c59274 c59275))
||5. (~ (tpp c59275 c59273))
||6. (pp c59275 c59273)
||7. (ec c59274 c59273)
||8. (ec c59275 c59274)
||
||> hyp
|=============================
|Step 13
|
|? (~ (o c59275 c59274))
|
|1. (p (f51952 c59274 c59275) c59274)
|2. (o c59274 c59275)
|3. (~ (ec c59274 c59275))
|4. (~ (tpp c59275 c59273))
|5. (pp c59275 c59273)
|6. (ec c59274 c59273)
|7. (ec c59275 c59274)
|
|> ((~ (o X Y)) <-- (ec X Y))
|=============================
|Step 14
|
|? (ec c59275 c59274)
|
|1. (o c59275 c59274)
|2. (p (f51952 c59274 c59275) c59274)
|3. (o c59274 c59275)
|4. (~ (ec c59274 c59275))
|5. (~ (tpp c59275 c59273))
|6. (pp c59275 c59273)
|7. (ec c59274 c59273)
|8. (ec c59275 c59274)
|
|> hyp
=============================
Step 15

? (ec c59274 c59273)

1. (~ (tpp c59275 c59273))
2. (pp c59275 c59273)
3. (ec c59274 c59273)
4. (ec c59275 c59274)

> hyp


LEMMA

Under ec/ec, converse proper part sharpens to converse tangential proper part.
=============================
Step 1

? (all x (all y (all z ((((ec x y) & (ec y z)) & (pp-1 x z)) => (tpp-1 x z)))))


> revsk
=============================
Step 2

? ((((~ (ec c66929 c66928)) v (~ (ec c66928 c66927))) v (~ (pp-1 c66929 c66927))) v (tpp-1 c66929 c66927))


> hypdisj
=============================
Step 3

? (tpp-1 c66929 c66927)

1. (pp-1 c66929 c66927)
2. (ec c66928 c66927)
3. (ec c66929 c66928)

> ((tpp-1 Y X) <-- (tpp X Y))
=============================
Step 4

? (tpp c66927 c66929)

1. (~ (tpp-1 c66929 c66927))
2. (pp-1 c66929 c66927)
3. (ec c66928 c66927)
4. (ec c66929 c66928)

> ((tpp Y Z) <-- (ec Y X) (ec X Z) (pp Y Z))
||=============================
||Step 5
||
||? (ec c66927 Var65)
||
||1. (~ (tpp c66927 c66929))
||2. (~ (tpp-1 c66929 c66927))
||3. (pp-1 c66929 c66927)
||4. (ec c66928 c66927)
||5. (ec c66929 c66928)
||
||> ((ec X Y) <-- (c X Y) (~ (o X Y)))
|||=============================
|||Step 6
|||
|||? (c c66927 Var65)
|||
|||1. (~ (ec c66927 Var65))
|||2. (~ (tpp c66927 c66929))
|||3. (~ (tpp-1 c66929 c66927))
|||4. (pp-1 c66929 c66927)
|||5. (ec c66928 c66927)
|||6. (ec c66929 c66928)
|||
|||> ((c Y X) <-- (c X Y))
|||=============================
|||Step 7
|||
|||? (c Var65 c66927)
|||
|||1. (~ (c c66927 Var65))
|||2. (~ (ec c66927 Var65))
|||3. (~ (tpp c66927 c66929))
|||4. (~ (tpp-1 c66929 c66927))
|||5. (pp-1 c66929 c66927)
|||6. (ec c66928 c66927)
|||7. (ec c66929 c66928)
|||
|||> ((c X Y) <-- (ec X Y))
|||=============================
|||Step 8
|||
|||? (ec Var65 c66927)
|||
|||1. (~ (c Var65 c66927))
|||2. (~ (c c66927 Var65))
|||3. (~ (ec c66927 Var65))
|||4. (~ (tpp c66927 c66929))
|||5. (~ (tpp-1 c66929 c66927))
|||6. (pp-1 c66929 c66927)
|||7. (ec c66928 c66927)
|||8. (ec c66929 c66928)
|||
|||> hyp
||=============================
||Step 9
||
||? (~ (o c66927 c66928))
||
||1. (~ (ec c66927 c66928))
||2. (~ (tpp c66927 c66929))
||3. (~ (tpp-1 c66929 c66927))
||4. (pp-1 c66929 c66927)
||5. (ec c66928 c66927)
||6. (ec c66929 c66928)
||
||> ((~ (o Y X)) <-- (~ (p (f59346 Y X) Y)))
||=============================
||Step 10
||
||? (~ (p (f59346 c66927 c66928) c66927))
||
||1. (o c66927 c66928)
||2. (~ (ec c66927 c66928))
||3. (~ (tpp c66927 c66929))
||4. (~ (tpp-1 c66929 c66927))
||5. (pp-1 c66929 c66927)
||6. (ec c66928 c66927)
||7. (ec c66929 c66928)
||
||> ((~ (p X Z)) <-- (p X Y) (~ (o Y Z)))
|||=============================
|||Step 11
|||
|||? (p (f59346 c66927 c66928) c66928)
|||
|||1. (p (f59346 c66927 c66928) c66927)
|||2. (o c66927 c66928)
|||3. (~ (ec c66927 c66928))
|||4. (~ (tpp c66927 c66929))
|||5. (~ (tpp-1 c66929 c66927))
|||6. (pp-1 c66929 c66927)
|||7. (ec c66928 c66927)
|||8. (ec c66929 c66928)
|||
|||> ((p (f59346 X Y) Y) <-- (o X Y))
|||=============================
|||Step 12
|||
|||? (o c66927 c66928)
|||
|||1. (~ (p (f59346 c66927 c66928) c66928))
|||2. (p (f59346 c66927 c66928) c66927)
|||3. (o c66927 c66928)
|||4. (~ (ec c66927 c66928))
|||5. (~ (tpp c66927 c66929))
|||6. (~ (tpp-1 c66929 c66927))
|||7. (pp-1 c66929 c66927)
|||8. (ec c66928 c66927)
|||9. (ec c66929 c66928)
|||
|||> hyp
||=============================
||Step 13
||
||? (~ (o c66928 c66927))
||
||1. (p (f59346 c66927 c66928) c66927)
||2. (o c66927 c66928)
||3. (~ (ec c66927 c66928))
||4. (~ (tpp c66927 c66929))
||5. (~ (tpp-1 c66929 c66927))
||6. (pp-1 c66929 c66927)
||7. (ec c66928 c66927)
||8. (ec c66929 c66928)
||
||> ((~ (o X Y)) <-- (ec X Y))
||=============================
||Step 14
||
||? (ec c66928 c66927)
||
||1. (o c66928 c66927)
||2. (p (f59346 c66927 c66928) c66927)
||3. (o c66927 c66928)
||4. (~ (ec c66927 c66928))
||5. (~ (tpp c66927 c66929))
||6. (~ (tpp-1 c66929 c66927))
||7. (pp-1 c66929 c66927)
||8. (ec c66928 c66927)
||9. (ec c66929 c66928)
||
||> hyp
|=============================
|Step 15
|
|? (ec c66928 c66929)
|
|1. (~ (tpp c66927 c66929))
|2. (~ (tpp-1 c66929 c66927))
|3. (pp-1 c66929 c66927)
|4. (ec c66928 c66927)
|5. (ec c66929 c66928)
|
|> ((ec X Y) <-- (c X Y) (~ (o X Y)))
||=============================
||Step 16
||
||? (c c66928 c66929)
||
||1. (~ (ec c66928 c66929))
||2. (~ (tpp c66927 c66929))
||3. (~ (tpp-1 c66929 c66927))
||4. (pp-1 c66929 c66927)
||5. (ec c66928 c66927)
||6. (ec c66929 c66928)
||
||> ((c Y X) <-- (c X Y))
||=============================
||Step 17
||
||? (c c66929 c66928)
||
||1. (~ (c c66928 c66929))
||2. (~ (ec c66928 c66929))
||3. (~ (tpp c66927 c66929))
||4. (~ (tpp-1 c66929 c66927))
||5. (pp-1 c66929 c66927)
||6. (ec c66928 c66927)
||7. (ec c66929 c66928)
||
||> ((c X Y) <-- (ec X Y))
||=============================
||Step 18
||
||? (ec c66929 c66928)
||
||1. (~ (c c66929 c66928))
||2. (~ (c c66928 c66929))
||3. (~ (ec c66928 c66929))
||4. (~ (tpp c66927 c66929))
||5. (~ (tpp-1 c66929 c66927))
||6. (pp-1 c66929 c66927)
||7. (ec c66928 c66927)
||8. (ec c66929 c66928)
||
||> hyp
|=============================
|Step 19
|
|? (~ (o c66928 c66929))
|
|1. (~ (ec c66928 c66929))
|2. (~ (tpp c66927 c66929))
|3. (~ (tpp-1 c66929 c66927))
|4. (pp-1 c66929 c66927)
|5. (ec c66928 c66927)
|6. (ec c66929 c66928)
|
|> ((~ (o Y X)) <-- (~ (p (f59346 Y X) Y)))
|=============================
|Step 20
|
|? (~ (p (f59346 c66928 c66929) c66928))
|
|1. (o c66928 c66929)
|2. (~ (ec c66928 c66929))
|3. (~ (tpp c66927 c66929))
|4. (~ (tpp-1 c66929 c66927))
|5. (pp-1 c66929 c66927)
|6. (ec c66928 c66927)
|7. (ec c66929 c66928)
|
|> ((~ (p X Z)) <-- (p X Y) (~ (o Y Z)))
||=============================
||Step 21
||
||? (p (f59346 c66928 c66929) c66929)
||
||1. (p (f59346 c66928 c66929) c66928)
||2. (o c66928 c66929)
||3. (~ (ec c66928 c66929))
||4. (~ (tpp c66927 c66929))
||5. (~ (tpp-1 c66929 c66927))
||6. (pp-1 c66929 c66927)
||7. (ec c66928 c66927)
||8. (ec c66929 c66928)
||
||> ((p (f59346 X Y) Y) <-- (o X Y))
||=============================
||Step 22
||
||? (o c66928 c66929)
||
||1. (~ (p (f59346 c66928 c66929) c66929))
||2. (p (f59346 c66928 c66929) c66928)
||3. (o c66928 c66929)
||4. (~ (ec c66928 c66929))
||5. (~ (tpp c66927 c66929))
||6. (~ (tpp-1 c66929 c66927))
||7. (pp-1 c66929 c66927)
||8. (ec c66928 c66927)
||9. (ec c66929 c66928)
||
||> hyp
|=============================
|Step 23
|
|? (~ (o c66929 c66928))
|
|1. (p (f59346 c66928 c66929) c66928)
|2. (o c66928 c66929)
|3. (~ (ec c66928 c66929))
|4. (~ (tpp c66927 c66929))
|5. (~ (tpp-1 c66929 c66927))
|6. (pp-1 c66929 c66927)
|7. (ec c66928 c66927)
|8. (ec c66929 c66928)
|
|> ((~ (o X Y)) <-- (ec X Y))
|=============================
|Step 24
|
|? (ec c66929 c66928)
|
|1. (o c66929 c66928)
|2. (p (f59346 c66928 c66929) c66928)
|3. (o c66928 c66929)
|4. (~ (ec c66928 c66929))
|5. (~ (tpp c66927 c66929))
|6. (~ (tpp-1 c66929 c66927))
|7. (pp-1 c66929 c66927)
|8. (ec c66928 c66927)
|9. (ec c66929 c66928)
|
|> hyp
=============================
Step 25

? (pp c66927 c66929)

1. (~ (tpp c66927 c66929))
2. (~ (tpp-1 c66929 c66927))
3. (pp-1 c66929 c66927)
4. (ec c66928 c66927)
5. (ec c66929 c66928)

> ((pp Y X) <-- (pp-1 X Y))
=============================
Step 26

? (pp-1 c66929 c66927)

1. (~ (pp c66927 c66929))
2. (~ (tpp c66927 c66929))
3. (~ (tpp-1 c66929 c66927))
4. (pp-1 c66929 c66927)
5. (ec c66928 c66927)
6. (ec c66929 c66928)

> hyp


LEMMA

Refine the overlap case to po, tpp, tpp-1, or equality.
=============================
Step 1

? (all x (all y (all z (((((ec x y) & (ec y z)) & (c x z)) & (o x z)) => ((((po x z) v (tpp x z)) v (tpp-1 x z)) v (e= x z))))))


> revsk
=============================
Step 2

? (((((~ (ec c74849 c74848)) v (~ (ec c74848 c74847))) v (~ (c c74849 c74847))) v (~ (o c74849 c74847))) v ((((po c74849 c74847) v (tpp c74849 c74847)) v (tpp-1 c74849 c74847)) v (e= c74849 c74847)))


> hypdisj
=============================
Step 3

? (e= c74849 c74847)

1. (~ (tpp-1 c74849 c74847))
2. (~ (tpp c74849 c74847))
3. (~ (po c74849 c74847))
4. (o c74849 c74847)
5. (c c74849 c74847)
6. (ec c74848 c74847)
7. (ec c74849 c74848)

> ((e= X Y) <-- (o X Y) (~ (po X Y)) (~ (pp X Y)) (~ (pp-1 X Y)))
|||=============================
|||Step 4
|||
|||? (o c74849 c74847)
|||
|||1. (~ (e= c74849 c74847))
|||2. (~ (tpp-1 c74849 c74847))
|||3. (~ (tpp c74849 c74847))
|||4. (~ (po c74849 c74847))
|||5. (o c74849 c74847)
|||6. (c c74849 c74847)
|||7. (ec c74848 c74847)
|||8. (ec c74849 c74848)
|||
|||> hyp
||=============================
||Step 5
||
||? (~ (po c74849 c74847))
||
||1. (~ (e= c74849 c74847))
||2. (~ (tpp-1 c74849 c74847))
||3. (~ (tpp c74849 c74847))
||4. (~ (po c74849 c74847))
||5. (o c74849 c74847)
||6. (c c74849 c74847)
||7. (ec c74848 c74847)
||8. (ec c74849 c74848)
||
||> hyp
|=============================
|Step 6
|
|? (~ (pp c74849 c74847))
|
|1. (~ (e= c74849 c74847))
|2. (~ (tpp-1 c74849 c74847))
|3. (~ (tpp c74849 c74847))
|4. (~ (po c74849 c74847))
|5. (o c74849 c74847)
|6. (c c74849 c74847)
|7. (ec c74848 c74847)
|8. (ec c74849 c74848)
|
|> ((~ (pp Y Z)) <-- (ec Y X) (ec X Z) (~ (tpp Y Z)))
|||=============================
|||Step 7
|||
|||? (ec c74849 Var39)
|||
|||1. (pp c74849 c74847)
|||2. (~ (e= c74849 c74847))
|||3. (~ (tpp-1 c74849 c74847))
|||4. (~ (tpp c74849 c74847))
|||5. (~ (po c74849 c74847))
|||6. (o c74849 c74847)
|||7. (c c74849 c74847)
|||8. (ec c74848 c74847)
|||9. (ec c74849 c74848)
|||
|||> hyp
||=============================
||Step 8
||
||? (ec c74848 c74847)
||
||1. (pp c74849 c74847)
||2. (~ (e= c74849 c74847))
||3. (~ (tpp-1 c74849 c74847))
||4. (~ (tpp c74849 c74847))
||5. (~ (po c74849 c74847))
||6. (o c74849 c74847)
||7. (c c74849 c74847)
||8. (ec c74848 c74847)
||9. (ec c74849 c74848)
||
||> hyp
|=============================
|Step 9
|
|? (~ (tpp c74849 c74847))
|
|1. (pp c74849 c74847)
|2. (~ (e= c74849 c74847))
|3. (~ (tpp-1 c74849 c74847))
|4. (~ (tpp c74849 c74847))
|5. (~ (po c74849 c74847))
|6. (o c74849 c74847)
|7. (c c74849 c74847)
|8. (ec c74848 c74847)
|9. (ec c74849 c74848)
|
|> hyp
=============================
Step 10

? (~ (pp-1 c74849 c74847))

1. (~ (e= c74849 c74847))
2. (~ (tpp-1 c74849 c74847))
3. (~ (tpp c74849 c74847))
4. (~ (po c74849 c74847))
5. (o c74849 c74847)
6. (c c74849 c74847)
7. (ec c74848 c74847)
8. (ec c74849 c74848)

> ((~ (pp-1 Y Z)) <-- (ec Y X) (ec X Z) (~ (tpp-1 Y Z)))
||=============================
||Step 11
||
||? (ec c74849 Var45)
||
||1. (pp-1 c74849 c74847)
||2. (~ (e= c74849 c74847))
||3. (~ (tpp-1 c74849 c74847))
||4. (~ (tpp c74849 c74847))
||5. (~ (po c74849 c74847))
||6. (o c74849 c74847)
||7. (c c74849 c74847)
||8. (ec c74848 c74847)
||9. (ec c74849 c74848)
||
||> hyp
|=============================
|Step 12
|
|? (ec c74848 c74847)
|
|1. (pp-1 c74849 c74847)
|2. (~ (e= c74849 c74847))
|3. (~ (tpp-1 c74849 c74847))
|4. (~ (tpp c74849 c74847))
|5. (~ (po c74849 c74847))
|6. (o c74849 c74847)
|7. (c c74849 c74847)
|8. (ec c74848 c74847)
|9. (ec c74849 c74848)
|
|> hyp
=============================
Step 13

? (~ (tpp-1 c74849 c74847))

1. (pp-1 c74849 c74847)
2. (~ (e= c74849 c74847))
3. (~ (tpp-1 c74849 c74847))
4. (~ (tpp c74849 c74847))
5. (~ (po c74849 c74847))
6. (o c74849 c74847)
7. (c c74849 c74847)
8. (ec c74848 c74847)
9. (ec c74849 c74848)

> hyp


LEMMA

Combine the dc/c split with the ec/o split and the refined overlap case.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (ec y z)) => (((dc x z) v (ec x z)) v ((((po x z) v (tpp x z)) v (tpp-1 x z)) v (e= x z)))))))


> revsk
=============================
Step 2

? (((~ (ec c83935 c83934)) v (~ (ec c83934 c83933))) v (((dc c83935 c83933) v (ec c83935 c83933)) v ((((po c83935 c83933) v (tpp c83935 c83933)) v (tpp-1 c83935 c83933)) v (e= c83935 c83933))))


> hypdisj
=============================
Step 3

? (e= c83935 c83933)

1. (~ (tpp-1 c83935 c83933))
2. (~ (tpp c83935 c83933))
3. (~ (po c83935 c83933))
4. (~ (ec c83935 c83933))
5. (~ (dc c83935 c83933))
6. (ec c83934 c83933)
7. (ec c83935 c83934)

> ((e= X Y) <-- (o X Y) (~ (po X Y)) (~ (pp X Y)) (~ (pp-1 X Y)))
|||=============================
|||Step 4
|||
|||? (o c83935 c83933)
|||
|||1. (~ (e= c83935 c83933))
|||2. (~ (tpp-1 c83935 c83933))
|||3. (~ (tpp c83935 c83933))
|||4. (~ (po c83935 c83933))
|||5. (~ (ec c83935 c83933))
|||6. (~ (dc c83935 c83933))
|||7. (ec c83934 c83933)
|||8. (ec c83935 c83934)
|||
|||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
||||=============================
||||Step 5
||||
||||? (c c83935 c83933)
||||
||||1. (~ (o c83935 c83933))
||||2. (~ (e= c83935 c83933))
||||3. (~ (tpp-1 c83935 c83933))
||||4. (~ (tpp c83935 c83933))
||||5. (~ (po c83935 c83933))
||||6. (~ (ec c83935 c83933))
||||7. (~ (dc c83935 c83933))
||||8. (ec c83934 c83933)
||||9. (ec c83935 c83934)
||||
||||> ((c X Y) <-- (~ (dc X Y)))
||||=============================
||||Step 6
||||
||||? (~ (dc c83935 c83933))
||||
||||1. (~ (c c83935 c83933))
||||2. (~ (o c83935 c83933))
||||3. (~ (e= c83935 c83933))
||||4. (~ (tpp-1 c83935 c83933))
||||5. (~ (tpp c83935 c83933))
||||6. (~ (po c83935 c83933))
||||7. (~ (ec c83935 c83933))
||||8. (~ (dc c83935 c83933))
||||9. (ec c83934 c83933)
||||10. (ec c83935 c83934)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (~ (ec c83935 c83933))
|||
|||1. (~ (o c83935 c83933))
|||2. (~ (e= c83935 c83933))
|||3. (~ (tpp-1 c83935 c83933))
|||4. (~ (tpp c83935 c83933))
|||5. (~ (po c83935 c83933))
|||6. (~ (ec c83935 c83933))
|||7. (~ (dc c83935 c83933))
|||8. (ec c83934 c83933)
|||9. (ec c83935 c83934)
|||
|||> hyp
||=============================
||Step 8
||
||? (~ (po c83935 c83933))
||
||1. (~ (e= c83935 c83933))
||2. (~ (tpp-1 c83935 c83933))
||3. (~ (tpp c83935 c83933))
||4. (~ (po c83935 c83933))
||5. (~ (ec c83935 c83933))
||6. (~ (dc c83935 c83933))
||7. (ec c83934 c83933)
||8. (ec c83935 c83934)
||
||> hyp
|=============================
|Step 9
|
|? (~ (pp c83935 c83933))
|
|1. (~ (e= c83935 c83933))
|2. (~ (tpp-1 c83935 c83933))
|3. (~ (tpp c83935 c83933))
|4. (~ (po c83935 c83933))
|5. (~ (ec c83935 c83933))
|6. (~ (dc c83935 c83933))
|7. (ec c83934 c83933)
|8. (ec c83935 c83934)
|
|> ((~ (pp Y Z)) <-- (ec Y X) (ec X Z) (~ (tpp Y Z)))
|||=============================
|||Step 10
|||
|||? (ec c83935 Var49)
|||
|||1. (pp c83935 c83933)
|||2. (~ (e= c83935 c83933))
|||3. (~ (tpp-1 c83935 c83933))
|||4. (~ (tpp c83935 c83933))
|||5. (~ (po c83935 c83933))
|||6. (~ (ec c83935 c83933))
|||7. (~ (dc c83935 c83933))
|||8. (ec c83934 c83933)
|||9. (ec c83935 c83934)
|||
|||> hyp
||=============================
||Step 11
||
||? (ec c83934 c83933)
||
||1. (pp c83935 c83933)
||2. (~ (e= c83935 c83933))
||3. (~ (tpp-1 c83935 c83933))
||4. (~ (tpp c83935 c83933))
||5. (~ (po c83935 c83933))
||6. (~ (ec c83935 c83933))
||7. (~ (dc c83935 c83933))
||8. (ec c83934 c83933)
||9. (ec c83935 c83934)
||
||> hyp
|=============================
|Step 12
|
|? (~ (tpp c83935 c83933))
|
|1. (pp c83935 c83933)
|2. (~ (e= c83935 c83933))
|3. (~ (tpp-1 c83935 c83933))
|4. (~ (tpp c83935 c83933))
|5. (~ (po c83935 c83933))
|6. (~ (ec c83935 c83933))
|7. (~ (dc c83935 c83933))
|8. (ec c83934 c83933)
|9. (ec c83935 c83934)
|
|> hyp
=============================
Step 13

? (~ (pp-1 c83935 c83933))

1. (~ (e= c83935 c83933))
2. (~ (tpp-1 c83935 c83933))
3. (~ (tpp c83935 c83933))
4. (~ (po c83935 c83933))
5. (~ (ec c83935 c83933))
6. (~ (dc c83935 c83933))
7. (ec c83934 c83933)
8. (ec c83935 c83934)

> ((~ (pp-1 Y Z)) <-- (ec Y X) (ec X Z) (~ (tpp-1 Y Z)))
||=============================
||Step 14
||
||? (ec c83935 Var55)
||
||1. (pp-1 c83935 c83933)
||2. (~ (e= c83935 c83933))
||3. (~ (tpp-1 c83935 c83933))
||4. (~ (tpp c83935 c83933))
||5. (~ (po c83935 c83933))
||6. (~ (ec c83935 c83933))
||7. (~ (dc c83935 c83933))
||8. (ec c83934 c83933)
||9. (ec c83935 c83934)
||
||> hyp
|=============================
|Step 15
|
|? (ec c83934 c83933)
|
|1. (pp-1 c83935 c83933)
|2. (~ (e= c83935 c83933))
|3. (~ (tpp-1 c83935 c83933))
|4. (~ (tpp c83935 c83933))
|5. (~ (po c83935 c83933))
|6. (~ (ec c83935 c83933))
|7. (~ (dc c83935 c83933))
|8. (ec c83934 c83933)
|9. (ec c83935 c83934)
|
|> hyp
=============================
Step 16

? (~ (tpp-1 c83935 c83933))

1. (pp-1 c83935 c83933)
2. (~ (e= c83935 c83933))
3. (~ (tpp-1 c83935 c83933))
4. (~ (tpp c83935 c83933))
5. (~ (po c83935 c83933))
6. (~ (ec c83935 c83933))
7. (~ (dc c83935 c83933))
8. (ec c83934 c83933)
9. (ec c83935 c83934)

> hyp


LEMMA

Reassociate the disjunctions into the target shape.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (ec y z)) => ((((((dc x z) v (ec x z)) v (po x z)) v (tpp x z)) v (tpp-1 x z)) v (e= x z))))))


> revsk
=============================
Step 2

? (((~ (ec c94187 c94186)) v (~ (ec c94186 c94185))) v ((((((dc c94187 c94185) v (ec c94187 c94185)) v (po c94187 c94185)) v (tpp c94187 c94185)) v (tpp-1 c94187 c94185)) v (e= c94187 c94185)))


> hypdisj
=============================
Step 3

? (e= c94187 c94185)

1. (~ (tpp-1 c94187 c94185))
2. (~ (tpp c94187 c94185))
3. (~ (po c94187 c94185))
4. (~ (ec c94187 c94185))
5. (~ (dc c94187 c94185))
6. (ec c94186 c94185)
7. (ec c94187 c94186)

> ((e= X Y) <-- (o X Y) (~ (po X Y)) (~ (pp X Y)) (~ (pp-1 X Y)))
|||=============================
|||Step 4
|||
|||? (o c94187 c94185)
|||
|||1. (~ (e= c94187 c94185))
|||2. (~ (tpp-1 c94187 c94185))
|||3. (~ (tpp c94187 c94185))
|||4. (~ (po c94187 c94185))
|||5. (~ (ec c94187 c94185))
|||6. (~ (dc c94187 c94185))
|||7. (ec c94186 c94185)
|||8. (ec c94187 c94186)
|||
|||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
||||=============================
||||Step 5
||||
||||? (c c94187 c94185)
||||
||||1. (~ (o c94187 c94185))
||||2. (~ (e= c94187 c94185))
||||3. (~ (tpp-1 c94187 c94185))
||||4. (~ (tpp c94187 c94185))
||||5. (~ (po c94187 c94185))
||||6. (~ (ec c94187 c94185))
||||7. (~ (dc c94187 c94185))
||||8. (ec c94186 c94185)
||||9. (ec c94187 c94186)
||||
||||> ((c X Y) <-- (~ (dc X Y)))
||||=============================
||||Step 6
||||
||||? (~ (dc c94187 c94185))
||||
||||1. (~ (c c94187 c94185))
||||2. (~ (o c94187 c94185))
||||3. (~ (e= c94187 c94185))
||||4. (~ (tpp-1 c94187 c94185))
||||5. (~ (tpp c94187 c94185))
||||6. (~ (po c94187 c94185))
||||7. (~ (ec c94187 c94185))
||||8. (~ (dc c94187 c94185))
||||9. (ec c94186 c94185)
||||10. (ec c94187 c94186)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (~ (ec c94187 c94185))
|||
|||1. (~ (o c94187 c94185))
|||2. (~ (e= c94187 c94185))
|||3. (~ (tpp-1 c94187 c94185))
|||4. (~ (tpp c94187 c94185))
|||5. (~ (po c94187 c94185))
|||6. (~ (ec c94187 c94185))
|||7. (~ (dc c94187 c94185))
|||8. (ec c94186 c94185)
|||9. (ec c94187 c94186)
|||
|||> hyp
||=============================
||Step 8
||
||? (~ (po c94187 c94185))
||
||1. (~ (e= c94187 c94185))
||2. (~ (tpp-1 c94187 c94185))
||3. (~ (tpp c94187 c94185))
||4. (~ (po c94187 c94185))
||5. (~ (ec c94187 c94185))
||6. (~ (dc c94187 c94185))
||7. (ec c94186 c94185)
||8. (ec c94187 c94186)
||
||> hyp
|=============================
|Step 9
|
|? (~ (pp c94187 c94185))
|
|1. (~ (e= c94187 c94185))
|2. (~ (tpp-1 c94187 c94185))
|3. (~ (tpp c94187 c94185))
|4. (~ (po c94187 c94185))
|5. (~ (ec c94187 c94185))
|6. (~ (dc c94187 c94185))
|7. (ec c94186 c94185)
|8. (ec c94187 c94186)
|
|> ((~ (pp Y Z)) <-- (ec Y X) (ec X Z) (~ (tpp Y Z)))
|||=============================
|||Step 10
|||
|||? (ec c94187 Var49)
|||
|||1. (pp c94187 c94185)
|||2. (~ (e= c94187 c94185))
|||3. (~ (tpp-1 c94187 c94185))
|||4. (~ (tpp c94187 c94185))
|||5. (~ (po c94187 c94185))
|||6. (~ (ec c94187 c94185))
|||7. (~ (dc c94187 c94185))
|||8. (ec c94186 c94185)
|||9. (ec c94187 c94186)
|||
|||> hyp
||=============================
||Step 11
||
||? (ec c94186 c94185)
||
||1. (pp c94187 c94185)
||2. (~ (e= c94187 c94185))
||3. (~ (tpp-1 c94187 c94185))
||4. (~ (tpp c94187 c94185))
||5. (~ (po c94187 c94185))
||6. (~ (ec c94187 c94185))
||7. (~ (dc c94187 c94185))
||8. (ec c94186 c94185)
||9. (ec c94187 c94186)
||
||> hyp
|=============================
|Step 12
|
|? (~ (tpp c94187 c94185))
|
|1. (pp c94187 c94185)
|2. (~ (e= c94187 c94185))
|3. (~ (tpp-1 c94187 c94185))
|4. (~ (tpp c94187 c94185))
|5. (~ (po c94187 c94185))
|6. (~ (ec c94187 c94185))
|7. (~ (dc c94187 c94185))
|8. (ec c94186 c94185)
|9. (ec c94187 c94186)
|
|> hyp
=============================
Step 13

? (~ (pp-1 c94187 c94185))

1. (~ (e= c94187 c94185))
2. (~ (tpp-1 c94187 c94185))
3. (~ (tpp c94187 c94185))
4. (~ (po c94187 c94185))
5. (~ (ec c94187 c94185))
6. (~ (dc c94187 c94185))
7. (ec c94186 c94185)
8. (ec c94187 c94186)

> ((~ (pp-1 Y Z)) <-- (ec Y X) (ec X Z) (~ (tpp-1 Y Z)))
||=============================
||Step 14
||
||? (ec c94187 Var55)
||
||1. (pp-1 c94187 c94185)
||2. (~ (e= c94187 c94185))
||3. (~ (tpp-1 c94187 c94185))
||4. (~ (tpp c94187 c94185))
||5. (~ (po c94187 c94185))
||6. (~ (ec c94187 c94185))
||7. (~ (dc c94187 c94185))
||8. (ec c94186 c94185)
||9. (ec c94187 c94186)
||
||> hyp
|=============================
|Step 15
|
|? (ec c94186 c94185)
|
|1. (pp-1 c94187 c94185)
|2. (~ (e= c94187 c94185))
|3. (~ (tpp-1 c94187 c94185))
|4. (~ (tpp c94187 c94185))
|5. (~ (po c94187 c94185))
|6. (~ (ec c94187 c94185))
|7. (~ (dc c94187 c94185))
|8. (ec c94186 c94185)
|9. (ec c94187 c94186)
|
|> hyp
=============================
Step 16

? (~ (tpp-1 c94187 c94185))

1. (pp-1 c94187 c94185)
2. (~ (e= c94187 c94185))
3. (~ (tpp-1 c94187 c94185))
4. (~ (tpp c94187 c94185))
5. (~ (po c94187 c94185))
6. (~ (ec c94187 c94185))
7. (~ (dc c94187 c94185))
8. (ec c94186 c94185)
9. (ec c94187 c94186)

> hyp


LEMMA

Finally prove the main theorem.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (ec y z)) => ((((((dc x z) v (ec x z)) v (po x z)) v (tpp x z)) v (tpp-1 x z)) v (e= x z))))))


> revsk
=============================
Step 2

? (((~ (ec c105605 c105604)) v (~ (ec c105604 c105603))) v ((((((dc c105605 c105603) v (ec c105605 c105603)) v (po c105605 c105603)) v (tpp c105605 c105603)) v (tpp-1 c105605 c105603)) v (e= c105605 c105603)))


> hypdisj
=============================
Step 3

? (e= c105605 c105603)

1. (~ (tpp-1 c105605 c105603))
2. (~ (tpp c105605 c105603))
3. (~ (po c105605 c105603))
4. (~ (ec c105605 c105603))
5. (~ (dc c105605 c105603))
6. (ec c105604 c105603)
7. (ec c105605 c105604)

> ((e= X Y) <-- (o X Y) (~ (po X Y)) (~ (pp X Y)) (~ (pp-1 X Y)))
|||=============================
|||Step 4
|||
|||? (o c105605 c105603)
|||
|||1. (~ (e= c105605 c105603))
|||2. (~ (tpp-1 c105605 c105603))
|||3. (~ (tpp c105605 c105603))
|||4. (~ (po c105605 c105603))
|||5. (~ (ec c105605 c105603))
|||6. (~ (dc c105605 c105603))
|||7. (ec c105604 c105603)
|||8. (ec c105605 c105604)
|||
|||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
||||=============================
||||Step 5
||||
||||? (c c105605 c105603)
||||
||||1. (~ (o c105605 c105603))
||||2. (~ (e= c105605 c105603))
||||3. (~ (tpp-1 c105605 c105603))
||||4. (~ (tpp c105605 c105603))
||||5. (~ (po c105605 c105603))
||||6. (~ (ec c105605 c105603))
||||7. (~ (dc c105605 c105603))
||||8. (ec c105604 c105603)
||||9. (ec c105605 c105604)
||||
||||> ((c X Y) <-- (~ (dc X Y)))
||||=============================
||||Step 6
||||
||||? (~ (dc c105605 c105603))
||||
||||1. (~ (c c105605 c105603))
||||2. (~ (o c105605 c105603))
||||3. (~ (e= c105605 c105603))
||||4. (~ (tpp-1 c105605 c105603))
||||5. (~ (tpp c105605 c105603))
||||6. (~ (po c105605 c105603))
||||7. (~ (ec c105605 c105603))
||||8. (~ (dc c105605 c105603))
||||9. (ec c105604 c105603)
||||10. (ec c105605 c105604)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (~ (ec c105605 c105603))
|||
|||1. (~ (o c105605 c105603))
|||2. (~ (e= c105605 c105603))
|||3. (~ (tpp-1 c105605 c105603))
|||4. (~ (tpp c105605 c105603))
|||5. (~ (po c105605 c105603))
|||6. (~ (ec c105605 c105603))
|||7. (~ (dc c105605 c105603))
|||8. (ec c105604 c105603)
|||9. (ec c105605 c105604)
|||
|||> hyp
||=============================
||Step 8
||
||? (~ (po c105605 c105603))
||
||1. (~ (e= c105605 c105603))
||2. (~ (tpp-1 c105605 c105603))
||3. (~ (tpp c105605 c105603))
||4. (~ (po c105605 c105603))
||5. (~ (ec c105605 c105603))
||6. (~ (dc c105605 c105603))
||7. (ec c105604 c105603)
||8. (ec c105605 c105604)
||
||> hyp
|=============================
|Step 9
|
|? (~ (pp c105605 c105603))
|
|1. (~ (e= c105605 c105603))
|2. (~ (tpp-1 c105605 c105603))
|3. (~ (tpp c105605 c105603))
|4. (~ (po c105605 c105603))
|5. (~ (ec c105605 c105603))
|6. (~ (dc c105605 c105603))
|7. (ec c105604 c105603)
|8. (ec c105605 c105604)
|
|> ((~ (pp Y Z)) <-- (ec Y X) (ec X Z) (~ (tpp Y Z)))
|||=============================
|||Step 10
|||
|||? (ec c105605 Var49)
|||
|||1. (pp c105605 c105603)
|||2. (~ (e= c105605 c105603))
|||3. (~ (tpp-1 c105605 c105603))
|||4. (~ (tpp c105605 c105603))
|||5. (~ (po c105605 c105603))
|||6. (~ (ec c105605 c105603))
|||7. (~ (dc c105605 c105603))
|||8. (ec c105604 c105603)
|||9. (ec c105605 c105604)
|||
|||> hyp
||=============================
||Step 11
||
||? (ec c105604 c105603)
||
||1. (pp c105605 c105603)
||2. (~ (e= c105605 c105603))
||3. (~ (tpp-1 c105605 c105603))
||4. (~ (tpp c105605 c105603))
||5. (~ (po c105605 c105603))
||6. (~ (ec c105605 c105603))
||7. (~ (dc c105605 c105603))
||8. (ec c105604 c105603)
||9. (ec c105605 c105604)
||
||> hyp
|=============================
|Step 12
|
|? (~ (tpp c105605 c105603))
|
|1. (pp c105605 c105603)
|2. (~ (e= c105605 c105603))
|3. (~ (tpp-1 c105605 c105603))
|4. (~ (tpp c105605 c105603))
|5. (~ (po c105605 c105603))
|6. (~ (ec c105605 c105603))
|7. (~ (dc c105605 c105603))
|8. (ec c105604 c105603)
|9. (ec c105605 c105604)
|
|> hyp
=============================
Step 13

? (~ (pp-1 c105605 c105603))

1. (~ (e= c105605 c105603))
2. (~ (tpp-1 c105605 c105603))
3. (~ (tpp c105605 c105603))
4. (~ (po c105605 c105603))
5. (~ (ec c105605 c105603))
6. (~ (dc c105605 c105603))
7. (ec c105604 c105603)
8. (ec c105605 c105604)

> ((~ (pp-1 Y Z)) <-- (ec Y X) (ec X Z) (~ (tpp-1 Y Z)))
||=============================
||Step 14
||
||? (ec c105605 Var55)
||
||1. (pp-1 c105605 c105603)
||2. (~ (e= c105605 c105603))
||3. (~ (tpp-1 c105605 c105603))
||4. (~ (tpp c105605 c105603))
||5. (~ (po c105605 c105603))
||6. (~ (ec c105605 c105603))
||7. (~ (dc c105605 c105603))
||8. (ec c105604 c105603)
||9. (ec c105605 c105604)
||
||> hyp
|=============================
|Step 15
|
|? (ec c105604 c105603)
|
|1. (pp-1 c105605 c105603)
|2. (~ (e= c105605 c105603))
|3. (~ (tpp-1 c105605 c105603))
|4. (~ (tpp c105605 c105603))
|5. (~ (po c105605 c105603))
|6. (~ (ec c105605 c105603))
|7. (~ (dc c105605 c105603))
|8. (ec c105604 c105603)
|9. (ec c105605 c105604)
|
|> hyp
=============================
Step 16

? (~ (tpp-1 c105605 c105603))

1. (pp-1 c105605 c105603)
2. (~ (e= c105605 c105603))
3. (~ (tpp-1 c105605 c105603))
4. (~ (tpp c105605 c105603))
5. (~ (po c105605 c105603))
6. (~ (ec c105605 c105603))
7. (~ (dc c105605 c105603))
8. (ec c105604 c105603)
9. (ec c105605 c105604)

> hyp
